data specification using nat recoveryentry := recovery-entry(. .pnum : nat;. .sqn : nat) ; variables rec : recoveryentry; end data specification